the_es:event_system{i:l}, e',e:es-E(the_es). (e  before(e'))  es-locl(the_es; e; e') 

latex

Definitions	x:A. B(x), before(e), t  T, prop{i:l}, P  Q, x. t(x), Y, if b then t else f fi , tt, ff, P  Q, P  Q, P  Q, P  Q, guard(T), wellfounded{i:l}(A; x,y.R(x;y)), x(s), , Unit, A, False, decidable(P),
Lemmas	es-locl-wellfnd, es-E wf, iff wf, l member wf, es-before wf, es-locl wf, es-first wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, event system wf, es-first-implies, decidable false, nil member, es-pred wf, es-pred-locl, iff functionality wrt iff, append wf, es-locl-iff, member append, or functionality wrt iff, cons member, false wf